﻿using System;
using System.Collections.Generic;
using System.Globalization;
using System.Linq;

namespace DiscreteMath
{
    /// <summary>
    /// Represents a deterministic automaton - a recognition device for regular languages. Abbreviated as DFA.
    /// A DFA transitions are always deterministic - for every letter in the alphabet and for every state of the automaton
    /// there exists a transition to a single state.
    /// </summary>
    public class DeterministicAutomaton : NondeterministicAutomaton
    {
        #region Constructors

        /// <summary>
        /// Initializes a new <see cref="NondeterministicAutomaton"/> with the specified states, 
        /// alphabet, transitions, starting state and final states.
        /// </summary>
        /// <param name="states">The set of states of the automaton.</param>
        /// <param name="alphabet">The set of letter the automaton's alphabet consists of.</param>
        /// <param name="transitions">The transitions that the automaton will follow when reading a word.</param>
        /// <param name="starting">The state that automaton will start in.</param>
        /// <param name="final">The set of states that the automaton considers final.</param>
        [System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1062:Validate arguments of public methods", 
            Justification = "Validation is done in FiniteStateMachine")]
        public DeterministicAutomaton(
            ISet<State> states,
            ISet<char> alphabet,
            Func<State, char, State> transitions,
            State starting,
            ISet<State> final) :
            base(states, alphabet, starting, final)
        {
            if (transitions == null)
                throw new ArgumentNullException("transitions");

            foreach (var letter in alphabet)
            {
                foreach (var state in states)
                {
                    var configuration = new Configuration(state, letter);
                    var transition = transitions(state, letter);
                    if (transition != null)
                    {
                        this.Transitions[configuration] = new HashSet<State>() { transition };
                    }
                    else
                    {
                        this.Transitions[configuration] = new HashSet<State>() { State.Undefined };
                    }
                }
            }

            this.RemoveUnreachableStates();
        }

        /// <summary>
        /// Initializes a new <see cref="NondeterministicAutomaton"/> with the specified states, 
        /// alphabet, transitions, starting state and final states.
        /// </summary>
        /// <param name="states">The set of states of the automaton.</param>
        /// <param name="alphabet">The set of letter the automaton's alphabet consists of.</param>
        /// <param name="transitions">The transitions that the automaton will follow when reading a word.</param>
        /// <param name="starting">The state that automaton will start in.</param>
        /// <param name="final">The set of states that the automaton considers final.</param>
        public DeterministicAutomaton(
            ISet<State> states,
            ISet<char> alphabet,
            IDictionary<Configuration, State> transitions,
            State starting,
            ISet<State> final) :
            base(states, alphabet, starting, final)
        {
            if (transitions == null)
                throw new ArgumentNullException("transitions");

            this.Transitions = new TransitionDictionary(transitions.ToDictionary(x => x.Key, x => (new HashSet<State> { x.Value } as ISet<State>)));

            this.RemoveUnreachableStates();
        }

        internal DeterministicAutomaton(
            ISet<State> states, 
            ISet<char> alphabet, 
            IDictionary<Configuration, ISet<State>> transitions, 
            State starting, 
            ISet<State> final) :
            base(states, alphabet, starting, final)
        {
            if (transitions == null)
                throw new ArgumentNullException("transitions");

            this.Transitions = new TransitionDictionary(transitions);
            this.RemoveUnreachableStates();
        }

        #endregion

        /// <summary>
        /// Produces the minimal (optimal) <see cref="DeterministicAutomaton"/> equivalent to the current one.
        /// </summary>
        /// <returns>A <see cref="DeterministicAutomaton"/> equivalent to the current one, with same number of states
        /// as the index of the Myhill-Nerod relation over the language accepted by the current automaton.</returns>
        public DeterministicAutomaton Minimize()
        {
            ISet<ISet<State>> equivalenceClasses = MergeNondistinguishableStates(this);
            ISet<State> states = new HashSet<State>(equivalenceClasses.Select(x => new State(x)));

            State starting = states.Single(x => x.Name.Contains(this.StartState.Name));
            ISet<State> final = new HashSet<State>(states.Where(state => 
            {
                return state.Name.ContainsAny(this.Final);
            }));

            TransitionDictionary transitions = new TransitionDictionary();
            foreach (ISet<State> equivalenceClass in equivalenceClasses)
            {
                var state = new State(equivalenceClass);
                foreach (char letter in this.Alphabet)
                {
                    State example = equivalenceClass.FirstOrDefault();
                    State exampleTransitsTo = this.Transitions[example, letter].FirstOrDefault();
                    if (exampleTransitsTo != State.Undefined)
                    {
                        ISet<State> transitsTo = equivalenceClasses.Single(x => x.Contains(exampleTransitsTo));
                        transitions.Add(state, letter, new HashSet<State>() { new State(transitsTo) });
                    }
                }
            }

            return new DeterministicAutomaton(states, this.Alphabet, transitions, starting, final);
        }

        private void RemoveUnreachableStates()
        {
            this.Total();
            ISet<State> reachable = new HashSet<State>() { this.StartState };
            this.AddReachableStates(reachable, this.StartState);
            State[] unreachable = this.States.Except(reachable).ToArray();
            this.States.ExceptWith(unreachable);
            IEnumerable<Configuration> unreachableTransitions = this.Transitions.Keys.Where(x => unreachable.Contains(x.State)).ToArray();
            foreach (Configuration key in unreachableTransitions)
            {
                this.Transitions.Remove(key);
            }
        }

        private void Total()
        {
            if (this.States.Contains(State.Undefined))
                return;

            bool shouldAddUndefined = false;
            foreach (char letter in this.Alphabet)
            {
                foreach (State state in this.States)
                {
                    if (this.Transitions[state, letter].FirstOrDefault() == State.Undefined)
                    {
                        shouldAddUndefined = true;
                        this.Transitions.Add(state, letter, new HashSet<State>() { State.Undefined });
                    }
                }
            }
            if (shouldAddUndefined)
            {
                var undefinedOnly = new HashSet<State>() { State.Undefined };
                this.States.Add(State.Undefined);
                foreach (var letter in this.Alphabet)
                {
                    this.Transitions.Add(State.Undefined, letter, undefinedOnly);
                }
            }
        }

        private void AddReachableStates(ISet<State> reachable, State from)
        {
            foreach (var letter in this.Alphabet)
            {
                foreach (var state in this.Transitions[from, letter])
                {
                    if (!reachable.Contains(state))
                    {
                        reachable.Add(state);
                        this.AddReachableStates(reachable, state);
                    }
                }
            }
        }

        private static ISet<ISet<State>> MergeNondistinguishableStates(DeterministicAutomaton automaton)
        {
            // Hopcroft, 1971, http://en.wikipedia.org/wiki/DFA_minimization
            var final = new HashSet<State>(automaton.Final);
            ISet<ISet<State>> p = new HashSet<ISet<State>>() { final, new HashSet<State>(automaton.States.Except(automaton.Final)) };
            ISet<ISet<State>> w = new HashSet<ISet<State>>() { final };

            while (w.Count != 0)
            {
                ISet<State> set = w.First();
                w.Remove(set);
                foreach (var letter in automaton.Alphabet)
                {
                    ISet<State> x = FindTransitionsTo(automaton, set, letter);
                    foreach (ISet<State> y in FindNonemptyIntersections(p, x))
                    {
                        p.Remove(y);
                        var intersection = new HashSet<State>(x.Intersect(y));
                        var difference = new HashSet<State>(y.Except(x));
                        p.Add(intersection);
                        p.Add(difference);

                        if (w.Contains(y))
                        {
                            w.Remove(y);
                            w.Add(intersection);
                            w.Add(difference);
                        }
                        else
                        {
                            if (intersection.Count() <= difference.Count())
                            {
                                w.Add(intersection);
                            }
                            else
                            {
                                w.Add(difference);
                            }
                        }
                    }
                }
            }

            return new HashSet<ISet<State>>(p.Where(x => x.Count != 0));
        }

        [System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1011:ConsiderPassingBaseTypesAsParameters",
            Justification = "This is method is only used when minimizing deterministic automata")]
        private static ISet<State> FindTransitionsTo(DeterministicAutomaton automaton, ISet<State> set, char letter)
        {
            ISet<State> transitions = new HashSet<State>();
            foreach (var state in automaton.States)
            {
                ISet<State> transition = automaton.Transitions[state, letter];
                if (transition.Count != 0)
                {
                    if (set.Contains(transition.First()))
                    {
                        transitions.Add(state);
                    }
                }
            }

            return transitions;
        }

        private static ISet<ISet<State>> FindNonemptyIntersections(ISet<ISet<State>> set, ISet<State> toIntersect)
        {
            ISet<ISet<State>> intersections = new HashSet<ISet<State>>();
            foreach (var item in set)
            {
                if (item.Overlaps(toIntersect))
                    intersections.Add(item);
            }
            return intersections;
        }

        /// <summary>
        /// Produces a <see cref="DeterministicAutomaton"/> that accepts the negation of the current DFA.
        /// </summary>
        /// <returns>A <see cref="DeterministicAutomaton"/> that recognizes the language that complements the language
        /// accepted by the current DFA.
        /// </returns>
        [System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1011:ConsiderPassingBaseTypesAsParameters",
            Justification = "Only an algorithm for negating a deterministic automaton is currently known")]
        public DeterministicAutomaton Negate()
        {
            var states = new HashSet<State>(this.States);
            var final = new HashSet<State>(this.States);
            final.ExceptWith(this.Final);

            return new DeterministicAutomaton(states, this.Alphabet, this.Transitions, this.StartState, final);
        }
        
        /// <summary>
        /// Produces a <see cref="DeterministicAutomaton"/> that accepts the intersection of the languages accepted
        /// by the current DFA and the one specified.
        /// </summary>
        /// <param name="automaton">The <see cref="DeterministicAutomaton"/> whose language to intersect with the language
        /// accepted by the current DFA.</param>
        /// <returns>A <see cref="DeterministicAutomaton"/> that accepts the language produced by intersecting the languages
        /// accepted by the current DFA and the one specified.</returns>
        public DeterministicAutomaton Intersection(DeterministicAutomaton automaton)
        {
            if (automaton == null)
                throw new ArgumentNullException("automaton");

            State renamedStarting;
            ISet<State> renamedStates, renamedFinals;
            TransitionDictionary renamedTransitions;
            Func<string, string> renamingFunction = (state) => state + "'";

            Algorithms.RenameDuplicates(this, automaton, renamingFunction, out renamedStates, out renamedStarting, out renamedFinals, out renamedTransitions);

            // Construct a second automaton whose states are renamed so that no conflicts with the current one occur.
            var secondAutomaton = new DeterministicAutomaton(renamedStates, automaton.Alphabet, renamedTransitions, renamedStarting, renamedFinals);
            State starting = FormatTuples(this.StartState, secondAutomaton.StartState);
            ISet<State> states = new HashSet<State>() { starting };
            ISet<State> final = new HashSet<State>();
            var alphabet = this.Alphabet.Union(automaton.Alphabet).ToSet();
            TransitionDictionary transitions = new TransitionDictionary();
            AddStates(this, secondAutomaton, this.StartState, secondAutomaton.StartState, states, final, transitions);

            var intersection = new DeterministicAutomaton(states, alphabet, transitions, starting, final);
            return intersection;
        }

        private static string FormatTuples(string first, string second)
        {
            return string.Format(CultureInfo.InvariantCulture, "<{0}, {1}>", first, second);
        }

        private static void AddStates(
            DeterministicAutomaton first, 
            DeterministicAutomaton second, 
            State currentStateFirst,
            State currentStateSecond,
            ISet<State> states, 
            ISet<State> final,
            TransitionDictionary transitions)
        {   
            State combined = FormatTuples(currentStateFirst, currentStateSecond);
            foreach (var letter in first.Alphabet)
            {
                State nextStateFirst = first.Transitions[currentStateFirst, letter].FirstOrDefault();
                State nextStateSecond = second.Transitions[currentStateSecond, letter].FirstOrDefault();
                ISet<State> nextStatesSet = new HashSet<State>();
                State nextState = State.Undefined;
                if (nextStateFirst != State.Undefined && nextStateSecond != State.Undefined)
                {
                    nextState = FormatTuples(nextStateFirst, nextStateSecond);
                }
                nextStatesSet.Add(nextState);

                if (!states.Contains(nextState))
                {
                    states.Add(nextState);
                    if (first.Final.Contains(nextStateFirst) && second.Final.Contains(nextStateSecond))
                    {
                        final.Add(nextState);
                    }
                    AddStates(first, second, nextStateFirst, nextStateSecond, states, final, transitions);
                }

                transitions.Add(combined, letter, nextStatesSet);
            }
        }

        public bool LanguageEquals(DeterministicAutomaton automaton)
        {
            if (automaton == null)
                throw new ArgumentNullException("automaton");

            if (!this.Alphabet.SetEquals(automaton.Alphabet))
                throw new InvalidOperationException("Both automata must work on the same alphabet");

            NondeterministicAutomaton first = this.Minimize();
            NondeterministicAutomaton second = automaton.Minimize();

            if (first.States.Count != second.States.Count)
                return false;

            IDictionary<State, State> stateMappings = new Dictionary<State, State>()
            {
                { first.StartState, second.StartState }
            };

            bool result =
                TestStatesForEquivalence(first, second, stateMappings, first.StartState, second.StartState); 
            
            return result;    
        }

        private static bool TestStatesForEquivalence(
            NondeterministicAutomaton first, 
            NondeterministicAutomaton second, 
            IDictionary<State, State> stateMappings, 
            State currentStateOfFirst, 
            State currentStateOfSecond)
        {
            foreach (char letter in first.Alphabet)
            {
                State nextStateOfFirst = first.Transitions[currentStateOfFirst, letter].FirstOrDefault();
                State nextStateOfSecond = second.Transitions[currentStateOfSecond, letter].FirstOrDefault();

                if (stateMappings.ContainsKey(nextStateOfFirst))
                {
                    if (stateMappings[nextStateOfFirst] != nextStateOfSecond)
                    {
                        return false;
                    }
                }
                else
                {
                    stateMappings[nextStateOfFirst] = nextStateOfSecond;
                    bool nextTest = 
                        TestStatesForEquivalence(first, second, stateMappings, nextStateOfFirst, nextStateOfSecond);

                    if (!nextTest)
                        return false;
                }
            }
            return true;
        }

        public static DeterministicAutomaton operator -(DeterministicAutomaton automaton)
        {
            if (automaton == null)
                throw new ArgumentNullException("automaton");

            return automaton.Negate();
        }

        /// <summary>
        /// Reads the given word and returns a value indicating whether the machine accepts it.
        /// </summary>
        /// <param name="word">The word to read.</param>
        /// <returns>
        ///   <c>True</c> if the machine accepts the word, <c>False</c> otherwise.
        /// </returns>
        /// <exception cref="System.ArgumentNullException">word</exception>
        public override bool ReadWord(IEnumerable<char> word)
        {
            if (word == null)
                throw new ArgumentNullException("word");

            if (word.Equals(SpecialSigns.EmptyWord.ToString()))
                return this.IsStartStateFinal;

            var currentState = StartState;
            foreach (var letter in word)
            {
                currentState = Transitions[currentState, letter].FirstOrDefault();
            }

            return Final.Contains(currentState);
        }
    }
}
